T:Type, L:(T List). hd(rev(L)) ~ last(L) 

latex

Definitions	hd(l), last(L), rev(as), Type, x:A. B(x), x:AB(x), type List, s ~ t
Lemmas	reverse-reverse, last-reverse, reverse wf